Nuprl Definition : sq_type
13,42
postcript
pdf
SQType(
T
) ==
x
,
y
:
T
. (
x
=
y
)
{
x
~
y
}
latex
clarification:
SQType(
T
) ==
x
:
T
,
y
:
T
. (
x
=
y
T
)
{
x
~
y
}
latex
Up
sqequal
1
,
sqequal
1
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
s
=
t
,
{
T
}
,
s
~
t
FDL editor aliases
sq_type
origin
x, y:T. (x = y) 
{x ~ y}
x:T, y:T. (x = y 
T) {x ~ y} x, y:T. (x = y) {x ~ y}
x:T, y:T. (x = y T) {x ~ y} x:A. B(x) Q